\documentclass[a4paper,12pt]{report} %размер бумаги устанавливаем А4, шрифт 12пунктов
\usepackage[T2A]{fontenc}
\usepackage[utf8]{inputenc}%включаем свою кодировку: koi8-r или utf8 в UNIX, cp1251 в Windows
\usepackage[english,russian]{babel}%используем русский и английский языки с переносами
\usepackage{amssymb,amsfonts,amsmath,mathtext,cite,enumerate,float} %подключаем нужные пакеты расширений
\usepackage[dvips]{graphicx} %хотим вставлять в диплом рисунки?
\usepackage{indentfirst}
\graphicspath{{images/}}%путь к рисункам

\makeatletter
\renewcommand{\@biblabel}[1]{#1.} % Заменяем библиографию с квадратных скобок на точку:
\makeatother

\usepackage{geometry} % Меняем поля страницы
\geometry{left=2cm}% левое поле
\geometry{right=1.5cm}% правое поле
\geometry{top=1cm}% верхнее поле
\geometry{bottom=2cm}% нижнее поле

\renewcommand{\theenumi}{\arabic{enumi}}% Меняем везде перечисления на цифра.цифра
%\renewcommand{\labelenumi}{\arabic{enumi}}% Меняем везде перечисления на цифра.цифра

\renewcommand{\theenumii}{.\arabic{enumii}}% Меняем везде перечисления на цифра.цифра
\renewcommand{\labelenumii}{\arabic{enumi}.\arabic{enumii}.}% Меняем везде перечисления на цифра.цифра

\renewcommand{\theenumiii}{.\arabic{enumiii}}% Меняем везде перечисления на цифра.цифра
\renewcommand{\labelenumiii}{\arabic{enumi}.\arabic{enumii}.\arabic{enumiii}.}% Меняем везде перечисления на цифра.цифра

\renewcommand{\thesection}{}
\begin{document}
\input{essay-title}% это титульный лист
\tableofcontents % это оглавление, которое генерируется автоматически
\newpage
%\chapter*{}
\section{Введение}
%\addtocounter{section}{1}
Для успешного использования симметричных криптосистем подобных \textit{DES} или \textit{Rijndael} возникает необходимость решения задачи распределения секретных ключей. Одним из способов решения является использование \textit{протоколов распределения с секретным ключом} (протокол широкоротой лягушки, Нидхейма-Шредера, Отвэй-Риса, Kerberos и др.). Общая идея, лежащая в их основе, состоит в следующем. Имеется некоторый доверенный центр; за каждым пользователем закрепляется долговременный секретный ключ, используя который он может связаться с доверенным центром (распределение долговременных ключей может осуществляться, например, физическим путем). Этот доверенный центр используется для генерации сеансовых ключей для обмена данными между любыми двумя пользователями каждый раз, когда в этом возникает необходимость.\\

Отличительная особенность данных протоколов состоит в том, что они по большей части весьма запутанны, и выявление их недостатков и уязвимостей является довольно тонким делом. Для того, чтобы упростить анализ протоколов распределения ключей, явным образом выделить их сходства и различия, а также предложить пути их улучшения, в 1989 году Бэрроузом, Абади и Нидхеймом была разработана формальная логика, именуемая ныне в честь ее авторов - \textit{BAN}-логика.

\section{Основная идея}
%\addtocounter{section}{1}
Основная идея \textit{BAN}-логики состоит в том, что при анализе протоколов в первую очередь стоит обратить внимание на восприятие сторонами поступающей информации - что они принимают на веру, а что им доподлинно известно или может быть выведено логическим путем из достоверных для них фактов (заметим, что даже при современных подходах к моделированию инфраструктуры открытых ключей (\textit{PKI}) эту идею берут на вооружение).\\

Формальный подход позволяет получить ответы, например, на следующие вопросы:
\begin{itemize}
\item[$\circ$]
Чего достигает данный протокол?
\item[$\circ$]
Необходимы ли дополнительные предположения для данного протокола?
\item[$\circ$]
Какие шаги являются лишними в данном протоколе?
\item[$\circ$]
Шифрует ли протокол какую-либо информацию, которую можно передавать в открытом виде?
\end{itemize}

Однако, стоит заметить, что \textit{BAN}-логика не предоставляет доказательства безопасности протокола; с ее помощью может быть построено лишь формальное доказательство его корректности.\\
\section{Обозначения}
\begin{itemize}
	\item[$\circ$] $P\mid \equiv X$ $(P\:\mathsf{believes}\:X)$ означает, что участник $P$ \textit{верит} в (или имеет право брать на веру) высказываение $X$, т.е. $P$ станет действовать так, как будто $X$ - истинная информация.
	\item[$\circ$] $P \triangleleft X$ $(P\:\mathsf{sees}\:X)$подразумевает, что $P$ \textit{видит} $X$, т.е. кто-то послал сообщение пользователю $P$, в котором содержится $X$. Так что $P$ может прочесть и воспроизвести $X$.
	\item[$\circ$] $P\mid \sim X$ $(P\:\mathsf{once\:said}\:X)$ означает, что $P$ однажды высказал $X$ и в тот момент верил в его истинность. Заметим, что здесь не уточняется время этого события.
	\item[$\circ$] $P\mid \Rightarrow X$ $(P\:\mathsf{has\:jurisdiction\:over}\:X)$ означает, что $X$ входит в юрисдикцию $P$, т.е. $P$ обладает властью над $X$ и по этому вопросу $P$ можно доверять.
	\item[$\circ$] $\sharp X$ $(\mathsf{fresh}(X))$ означает, что высказывание $X$ получено недавно. Этот символ используется обычно для числовых вставок.
	\item[$\circ$]  $P \stackrel{k}{\longleftrightarrow} Q$ означает, что $P$ и $Q$ используют для общения \textit{разделенный
ключ} $k$. Предполагается, что ключ достаточно стоек и не может быть раскрыт никем из посторонних, если это не предусмотрено протоколом.
	\item[$\circ$] Обозначение $\lbrace X \rbrace_k$ обычно подразумевает, что данные $X$ зашифрованы ключом $k$. Шифрование считают совершенным, в частности $X$ остается зачекреченным до тех пор, пока одна из сторон сознательно не раскроет его в какой-то другой части протокола.
\end{itemize}

	Кроме того, вместо обычной операции <<И>> употребляется запятая, а запись  $\frac{A,B}{C}$ означает, что из истинности утверждений $A$ и $B$ следует истинность высказывания $C$. Такой способ символьного изображения сложных
конструкций принят во многих формальных логиках.\\

\textit{Замечание}. Символьные обозначения были предложены авторами в оригинальной работе. Используемые здесь и ниже англоязычные обозначения не являются общепринятыми, однако упрощают восприятие формул.
\section{Правила вывода}

\textit{BAN}-логика опирается на множество постулатов или правил вывода. Разберем лишь главные из них.\\

\textit{Правило о значении сообщения:}\\

\begin{equation}
\frac{A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B, A\:\mathsf{sees}\:\lbrace X \rbrace_K}{A\:\mathsf{believes}\:B\:\mathsf{once\:said}\:X}
\end{equation}

Эквивалентная словесная формулировка: из предположений о том, что $A$ верит в совместное использование ключа $K$ с $B$, и $A$ видит сообщение $X$, зашифрованное ключом $K$, мы делаем вывод: $A$ верит, что $B$ в какой-то момент высказал $X$. Заметим, что здесь неявно предполагается, что сам $A$ никогда не высказывал $X$.\\

\textit{Правило проверки уникальности числовых вставок:}
\begin{equation}
\frac{A\:\mathsf{believes}\:\mathsf{fresh}(X), A\:\mathsf{believes}\:B\:\mathsf{once\:said}\:X}{A\:\mathsf{believes}\:B\:\mathsf{believes}\:X}
\end{equation}
т.е. если $A$ верит в новизну $X$ и в то, что $B$ когда-то высказал $X$, то $A$ верит, что $B$ по-прежнему доверяет $X$.\\

\textit{Правило юрисдикции:}
\begin{equation}
\frac{A\:\mathsf{believes}\:B\:\mathsf{has\:jurisdiction\:over}\:X, A\:\mathsf{believes}\:B\:\mathsf{believes}\:X}{A\:\mathsf{believes}\:X}
\end{equation}
говорит, что если $A$ верит в полномочия $B$ относительно $X$, т.е. $A$ полагается на $B$ в деле с $X$, и $A$ верит в то, что $B$ верит в $X$, то $A$ должен верить в $X$.\\

\textit{Другие правила.} Оператор доверия и запятая, разделяющая высказывания, рассматриваемые совместно, подчиняются следующим соотношениям:

\begin{equation}
\frac{P\:\mathsf{believes}\:X, P\:\mathsf{believes}\:Y}{P\:\mathsf{believes}\:(X,Y)}
\end{equation}

\begin{equation}
\frac{P\:\mathsf{believes}\:(X,Y)}{P\:\mathsf{believes}\:X}
\end{equation}

\begin{equation}
\frac{P\:\mathsf{believes}\:Q\:\mathsf{believes}\:(X,Y)}{P\:\mathsf{believes}\:Q\:\mathsf{believes}\:X}
\end{equation}

Оператор <<однажды высказал>> удовлетворяет аналогичному соотношению:
\begin{equation}
\frac{P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:(X,Y)}{P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:X}
\end{equation}

Заметим, что предположения $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:X$ и $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:Y$ не влекут утверждения $P\:\mathsf{believes}\:Q\:\mathsf{once\:said}\:(X,Y)$, поскольку последнее означает, что $Q$ произнес $X$ и $Y$ в одно и то же время. Наконец, если какая-то часть высказывания получена недавно, то это же можно утверждать и про всю конструкцию:
\begin{equation}
\frac{P\:\mathsf{believes}\;\mathsf{fresh}\:X}{P\:\mathsf{believes}\;\mathsf{fresh}\:(X,Y)}
\end{equation}
\section{Формальный подход к анализу протоколов}
В терминах \textit{BAN}-логики, цели исследуемого протокола состоят как минимум в следующем:
\begin{equation}
A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
т.е. оба участника должны поверить в то, что они нашли секретный ключ для обмена друг с другом закрытой информацией.\\

Однако можно было бы потребовать и большего, например,
\begin{equation}
A\:\mathsf{believes}\:B\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\:A\:\mathsf{believes}\:A \stackrel{K}{\longleftrightarrow} B
\end{equation}
что обычно называют подтверждением приема ключа. Иначе говоря, можно считать, что в результате работы протокола $A$ будет уверен в знании $B$ о том, что он разделяет секретный ключ с $A$, а $B$ верит в то, что и $A$ знает об их обшем ключе.\\

Формальное исследование протокола можно разбить на 4 этапа:
\begin{enumerate}
\item 
Перевести реальный протокол в идеализованный.
\item
Записать начальные предположения протокола.
\item
Присоединить логические формулы к предложениям, получая утверждения о состоянии системы после каждого предложения.
\item
Применить логические постулаты к утверждениям и предположениям.
\end{enumerate}

\section{Анализ протокола широкоротой лягушки}
Для наглядности, чтобы понять, как это все работает <<в реальной жизни>>, подвергнем анализу протокол широкоротой лягушки,
использующий синхронизацию часов.\\

Напомним, что он состоит из обмена двумя сообщениями:\\
\begin{equation}
A \longrightarrow S:A,\lbrace t_a,b,k_{ab} \rbrace_{k_{ab}}
\end{equation}
\begin{equation}
S \longrightarrow B:\lbrace t_s,a,k_{ab} \rbrace_{k_{bs}}
\end{equation}

При идеализации это выглядит так:
\begin{equation}
A \longrightarrow S: \lbrace t_a, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{as}}
\end{equation}
\begin{equation}
S \longrightarrow B: \lbrace t_s, A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}
\end{equation}

Идеализированное первое сообщение говорит $S$, что\\
\begin{list}{-}{}
\item $t_a$ - временн\'{а}я или числовая вставка,
\item $k_{ab}$ - ключ, который прeдлагаeтся использовать для коммуникации с $B$.
\end{list}
Итак, какие предположения сделаны в начале работы протокола? Ясно, что $A$, $B$ и $S$ используют секретные ключи для обмена шифрованными сообщениями друг с другом, что на языке $BAN$-логики может быть выражено как
\begin{equation}
A\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: B\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: B\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
Есть два предположения о временн\'{ы}х вставках:
\begin{equation}
S \:\mathsf{believes}\: \mathsf{fresh}\:t_a
\end{equation}
\begin{equation}
B \:\mathsf{believes}\: \mathsf{fresh}\:t_s
\end{equation}
и еще три предположения:
\begin{list}{-}{}
\item $B$ полагается на $A$ в выборе хорошего ключа:
\begin{equation}
B \:\mathsf{believes}\: (A\:\mathsf{has\:jurisdiction\:over}A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\item $B$ доверяет $S$ передать ключ от $A$:
\begin{equation}
B \:\mathsf{believes}\: (S\:\mathsf{has\:jurisdiction\:over}A \:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\item $A$ верит, что сеансовый ключ принят:\\
\begin{equation}
A \:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\end{list}
Обратим внимание на то, как последние предположения обнажают известные проблемы, связанные с данным протоколом.\\

Опираясь на сделанные предположения, мы можем проанализировать протокол. Посмотрим, какой вывод можно сделать из первого сообщения $A \longrightarrow S:A,\lbrace t_a,B,k_{ab} \rbrace_{k_{as}}$.
\begin{list}{-}{}
\item $S$, видя сообщение, зашифрованное ключом $k_{as}$, может сделать вывод о том, что оно послано клиентом $A$.
\item Наличие свежей временной вставки $t_a$ позволяет участнику $S$ заключить, что и все сообщение написано недавно.
\textsl{\item} Из свежести всего сообщения $S$ выводит, что клиент $A$ верил в то, что послал.
\item Следовательно,
\begin{equation}
S \:\mathsf{believes}\:A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
т.е. $S$ подготовлен к посылке второго сообщения протокола.
\end{list}

Обратимся к следующему этапу: $S \longrightarrow B: \lbrace t_s, A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}$
\begin{list}{-}{}
\item Увидев послание, зашифрованное ключом $k_{bs}$, клиент $В$ понимает,
что оно было отправлено $S$.
\item Временн\'{а}я вставка $t_s$ доказывает $B$, что все сообщение было
послано только что.
\item Ввиду свежести сообщения, $B$ заключает, что $S$ доверяет всему
посланному.
\item В частности, $B$ верит в то, что $S$ доверяет второй части сообщения.
\item Но $B$ верит и в то, что в юрисдикцию $S$ входит выяснить, знает ли его партнер $А$ секретный ключ, и поэтому $B$ вверяет $A$ полномочия по генерированию ключа.
\end{list}
Из этих рассуждений можно сделать вывод:
\begin{equation}
B\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: A\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
Комбинируя это с исходным предположением: $A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B$, получаем, что анализируемый протокол распределения ключей обоснован. Единственное, чего мы не встретили в нем, это
\begin{equation}
A\:\mathsf{believes}\: B\:\mathsf{believes}\:A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
т.е. А не добился подтверждения тому, что В получил нужный ключ.\\

Обратим внимание на то, что применение \textit{BAN}-логики к анализу формализовало все этапы протокола, так что их стало легче
сравнивать с предположениями, необходимыми любому протоколу для работы. Кроме того, этот формализм проясняет точки зрения на работу протокола всех его участников.
\section{Анализ протокола Kerberos}
В протоколе Kerberos происходит обмен следующими сообщениями:
\begin{equation}
A \longrightarrow S: A,B
\end{equation}
\begin{equation}
S \longrightarrow A:\lbrace t_s, l, k_{ab}, B, \lbrace t_s, l, k_{ab}, A \rbrace_{k_{bs}} \rbrace_{k_{as}}
\end{equation}
\begin{equation}
A \longrightarrow B:\lbrace t_s, l, k_{ab}, A \rbrace_{k_{bs}},\lbrace A, t_a \rbrace_{k_{ab}}
\end{equation}
\begin{equation}
B \longrightarrow A:\lbrace t_a+1\rbrace_{k_{ab}}
\end{equation}

Здесь $t_a$, $t_s$ - отметки времени, $l$ - время жизни. Идеализованный протокол выглядит следующим образом:
\begin{equation}
S \longrightarrow A: \lbrace t_s, A \stackrel{k_{ab}}{\longleftrightarrow} B, \lbrace t_s, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}} \rbrace_{k_{as}}
\end{equation}
\begin{equation}
A \longrightarrow B:\lbrace t_s, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}, \lbrace t_a, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{ab}}\:from\:A
\end{equation}
\begin{equation}
B \longrightarrow A:\lbrace t_a,A \stackrel{k_{ab}}{\longleftrightarrow} B\rbrace_{k_{ab}}\:from\:B
\end{equation}
Первое сообщение опущено, поскольку это не изменяет логические свойства протокола. Также для простоты время жизни $l$ объединено с меткой $t_s$.\\

Запишем предположения протокола:
\begin{equation}
A\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: B\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: A\stackrel{k_{as}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: B\stackrel{k_{bs}}{\longleftrightarrow} S
\end{equation}
\begin{equation}
S\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
A \:\mathsf{believes}\: (S\:\mathsf{has\:jurisdiction\:over}A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\begin{equation}
B \:\mathsf{believes}\: (S\:\mathsf{has\:jurisdiction\:over}A\stackrel{k_{ab}}{\longleftrightarrow} B)
\end{equation}
\begin{equation}
A \:\mathsf{believes}\: \mathsf{fresh}\:t_s
\end{equation}
\begin{equation}
B \:\mathsf{believes}\: \mathsf{fresh}\:t_s
\end{equation}
\begin{equation}
B \:\mathsf{believes}\: \mathsf{fresh}\:t_a
\end{equation}

Из трех последних предположений очевидно, что протокол опирается на использование синхронизованных часов, поскольку каждый пользователь верит в свежесть временных меток.\\

После того, как $A$ получает первое сообщение (идеализованного) протокола, имеем:\\
\begin{equation}
A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
A\:\mathsf{sees}\: \lbrace t_s, A \stackrel{k_{ab}}{\longleftrightarrow} B \rbrace_{k_{bs}}
\end{equation}

$A$ передает зашифрованное сообщение от сервера аутентификации вместе с другим сообщением, содержащим метку времени. Изначально, $B$ может расшифровать только одну часть:\\
\begin{equation}
B\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}

Знание нового ключа позволяет $B$ расшифровать остаток сообщения; после этого получаем:\\
\begin{equation}
B\:\mathsf{believes}\:A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}

Последнее сообщение убеждает $A$ в том, что $B$ доверяет ключу и последнему полученному от $A$ сообщению. Окончательный результат следующий:\\
\begin{equation}
A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
A\:\mathsf{believes}\:B\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}
\begin{equation}
B\:\mathsf{believes}\:A\:\mathsf{believes}\: A\stackrel{k_{ab}}{\longleftrightarrow} B
\end{equation}

Как уже было указано, ключевое предположение протокола состоит в том, что часы пользователей синхронизованы с сервером. На практике, это достигается путем синхронизации на короткое время (порядка нескольких минут) с защищенным центром синхронизации. Также заметим, что окончательный результат относительно доверия участников может быть получен без использования дополнительного шифрования в первом сообщении.\\

\section{Заключение}

Авторы \textit{BAN}-логики рассматривают идеализированные протоколы как более ясные и понятные описания, чем традиционные. Это действие часто подвергается критике, так как в процессе формализации реальный протокол может быть искажен. Более того, ряд критиков пытается показать, что \textit{BAN}-логика может получить и очевидно неправильные характеристики протоколов. Это связано с тем, что \textit{BAN}-логика, по существу, занимается доверием, а не безопасностью.\\

Несмотря на эту критику \textit{BAN}-логика достигла определенных успехов. Ей удалось обнаружить "дыры" в нескольких протоколах, включая протокол Нидхейма-Шредера и раннюю черновую версию протокола CCITT X.509. Также она обнаружила избыточность во многих протоколах, включая Yahalom и Kerberos. Во многих работах \textit{BAN}-логика используется для заявления претензии о безопасности описываемых протоколов.\\

Многие другие логические системы были разработаны как расширения \textit{BAN}-логики, например, с вероятностным или меняющимся во времени доверием.
%\section{Литература}
\begin{thebibliography}{99}
\bibitem{originalpaper} M. Burrows, M. Abadi, R. Needham. A Logic of Authentication. Systems Research Center of Digital Equipment Corporation in Palo Alto, California, 1989.
\bibitem{smart} Н. Смарт. Криптография. Москва, Техносфера, 2006, стр. 162-179.
\bibitem{alferov} А. Алферов, А. Кузьмин, А. Зубов, А. Черемушкин. Основы криптографии. Москва, Гелиос АРВ, 2002, стр. 378-385, 404-406.
\bibitem{schneier} B. Schneier. Applied Cryptography. Second Edition, John Wiley \& Sons, 1996, стр. 66-69.
\end{thebibliography}

\end{document}
